\chapter{Logical Time}
\section{Question 1 Design a logical-time base algorithm}
Posons les variables du processus suivantes : 

\begin{itemize}
\item  \verb+ListMessages+ : représente la liste des messages qui ont été reçus mais pas délivrés.
\item \verb+m.i+ indique l'identifiant du processus à l'origine du message.
\item \verb+m.sn+ indique le prédécesseur du message envoyé par le processus émetteur.
\item \verb+m.cb+ Liste des prédécesseurs du message.
\end{itemize}

\begin{algorithm}
  \caption{\textbf{CO\_Receive}(Message m)}
  \label{algo:receive}
  \begin{algorithmic}[1]
    \IF{ $\forall$ p$\in$ m.cb $\mid$ p.sn $\leq$ del(p.i)}
    \STATE  del(m.i) ++
    \STATE  cb +=\{m.sn, m.i\}
    \STATE  CO\_Deliver(m)
    \FORALL{m\'~ $\in$ ListMessages}
    \STATE CO\_Receive2(m')
    \ENDFOR
    \ELSE
    \STATE ListMessages.add(m)
    \ENDIF
  \end{algorithmic}
\end{algorithm}


La fonction \verb+CO_Receive2(Message m)+ est la fonction suivante : 
\begin{algorithm}
  \caption{\textbf{CO\_Receive2}( Message m)}
  %/* \textit{ où pred est la liste des prédécesseurs */}
  \label{algo:receive2}
  \begin{algorithmic}[1]
    \IF{ $\forall$ p$\in$ m.cb $\mid$ p.sn $\leq$ del(p.i)}
    \STATE  del(m.i) ++
    \STATE  cb +=\{m.sn, m.i\}
    \STATE  CO\_Deliver(m)
    \STATE  ListMessage.delete(m)
    \FORALL{ m\'~ $\in$ ListMessages}
    \STATE CO\_Receive2(m\'~)
    \ENDFOR
    \ENDIF
  \end{algorithmic}
\end{algorithm}


\section{Question 2 Analyse of the algorithm}

Les valeurs que peuvent prendre \verb+cb+ sont les suivantes :

\begin{description}
\item[Minimum] \hfill \\
  C'est la valeur 1 : (\cf{} figure \ref{fig:min} : le message \verb+m1+ n'a qu'un seul prédécesseur).
\item[Maximum] \hfill \\
  C'est le nombre de processus (\cf{} figure \ref{fig:max}: le message \verb+m3+ aura trois prédécesseurs). Cette borne est possible grâce à la mise à jour de la variable.
\end{description}

\begin{figure}[htb]
  \setlength{\unitlength}{0.8mm}
  \begin{subfigure}[b]{0.5\textwidth}
    \begin{picture}(60,40)
      \put(20,20){\vector(1,0){80}}
      \put(40,20){\circle*{2}}
      \put(20,0){\vector(1,0){80}}
      \put(40,20){\vector(3,-2){29,7}}
      \put(35,22){\shortstack[l]{m1}}
    \end{picture}
    \caption{Valeur minimum}
    \label{fig:min}
  \end{subfigure}%
  ~ %add desired spacing between images, e. g. ~, \quad, \qquad etc. 
  %(or a blank line to force the subfigure onto a new line)
  \begin{subfigure}[b]{0.5\textwidth}
    \begin{picture}(60,40)
    \put(10,20){\vector(1,0){80}}
    \put(20,20){\circle*{2}}
    \put(10,22){\shortstack[l]{m1}}
    \put(20,20){\vector(3,-2){14.8}}
    \put(10,0){\vector(1,0){80}}
    \put(10,10){\vector(1,0){80}}
    \put(20,20){\vector(3,-2){14.8}}

    \put(20,20){\vector(1,-4){5}}
    \put(45,10){\circle*{2}}
    \put(37,11){\shortstack[l]{m2}}
    \put(45,10){\vector(1,2){5}}
    \put(45,10){\vector(1,-2){5}}

    \put(70,0){\circle*{2}}
    \put(62,1){\shortstack[l]{m3}}
    \end{picture}
    \caption{Valeur maximum}
    \label{fig:max}
  \end{subfigure}
  \caption{Valeurs aux bornes de cb}\label{fig:valeurs}
\end{figure}

Regardons si les propriétés citées dans le paragraphe 2.1 de l'énonce est vérifiée : 

\begin{description}
\item[Validité] Les canaux étant sûr, aucun messages de ne peut être \og perdu \fg{}. En effet il n'y a pas de parasites dans les canaux.
\item[Intégrité] Dans l'algorithme \ref{algo:receive} si un message est reçu et qu'il est délivré immédiatement alors il n'est lu qu'une fois. Au contraire s'il n'est pas délivré il est mis en attente et sera supprimé dès qu'il sera délivré (\emph{cf.} ligne de l'algorithme \ref{algo:receive2}).
\item[CO\_Delivery] Cette propriété est vérifiée grâce à la condition à la ligne de l'algorithme \ref{algo:receive}.
\item[Terminaison] On ne peut pas perdre de messages car les canaux sont sûr.
\end{description}






% LocalWords:  Logical Time logical-time algorithm ListMessages m.i
% LocalWords:  m.sn m.cb pseudo-code CO Receive p.sn del p.i cb aa of
% LocalWords:  Deliver ListMessages.add ListMessage.delete the blah
% LocalWords:  Delivery

